… both channel and engine API

Replace PendingWork/ProcessingContext split with a flat List[WorkItem]
queue where engine API calls and local Emerald state updates are
interleaved as equal work items. This generalizes naturally to apps
talking to multiple external components.

Key changes:
- WorkItem sum type: EngineCall | FinalizeGetValue | FinalizeReceivedProposal | FinalizeDecided
- pendingWork: List[WorkItem] replaces Option[PendingWork]
- stepAdvanceWork processes one item per step with uniform queue pop
- Handlers renamed handle* → finalize* to reflect they update Emerald state
- Stale proposal check moved to stepReceivedProposal (before enqueueing)
- Removed rethUnchanged alias, PendingWork type, ProcessingContext type
- Added TODOs for EngineCallSpec boilerplate and state separation

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

- Categorize invariants by scope: Emerald-only, Emerald↔Malachite,
  Emerald↔Reth
- Remove chain_continuity_inv (Reth contract property, duplicated from
  reth::contractInv)
- Add commented channelContractInv/engineContractInv for full contract
  verification
- Update independent crash TODO with concrete design: deadlock analysis,
  work queue clearing, validated_cache handling, invariant gating on
  Reth phase

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

- Add biasedStep action to witnesses module: restricts node selection to
  nodes with last_decided_height < 1 until all nodes complete height-1,
  correcting the probabilistic starvation that prevents uniform random
  simulation from finding the witness
- Add allKnownProposals helper to derive proposal set from Emerald state,
  avoiding the need for gen:: which is not re-exported from the composition
- Update canDecideTwoHeights_debug_report.md: correct diagnosis (uniform
  random walk starvation, not scheduler preference), add round-timeout
  analysis, add Biased Step section with confirmed violation result

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>